| Definitions |  x:A. B(x), P   Q, t  T,  , P  Q, P  Q, P & Q, P Q, sender(e), index(e),  x:A. B(x),  , time(e), e <loc e', loc(e), t.1, t.2, p = q, rcvs(l;t),  T, True,  b, isrcv(l;a), p   q,  b, tt, if b then t else f fi , ff, False, snds(l;t), {i..j }, i  j < k, S  T, {T}, concat(ll), map(f;as), m(l;t), upto(n), Y, SQType(T), Top, reduce(f;k;as), A B, A,  , Unit, E, kind(e), act(e), Dec(P),  |
| Lemmas | fair-fifo wf, world wf, IdLnk wf, lnk wf, assert wf, isrcv wf, w-ekind wf, w-E wf, iff functionality wrt iff, w-locl wf, w-sender wf, w-index wf, int seg wf, length wf1, w-Msg wf, w-sends wf, w-eq-E wf, or functionality wrt iff, and functionality wrt iff, assert-w-eq-E-iff, w-match-exists, mu-property, w-match wf, w-time wf, nat wf, le wf, mu wf, implies functionality wrt iff, iff wf, Id wf, w-loc wf, lsrc wf, band wf, eq id wf, eq int wf, w-action wf, ldst wf, w-rcvs wf, w-snds wf, iff transitivity, assert of band, assert-eq-id, assert of eq int, assert-w-match, w-isrcvl wf, w-a wf, rcv?-kind, w-info wf, w-kind-lemma, w-loc-lemma, w-loc-rcv, squash wf, true wf, rcv?-link, w-isnull wf, bool wf, eqtt to assert, bnot wf, not wf, eqff to assert, assert of bnot, w-kind wf, assert-eq-lnk, filter map upto, decidable lt, iseg length, concat wf, map wf, w-ml wf, upto wf, concat iseg, iseg map, upto iseg, not functionality wrt iff, map append sq, concat append, top wf, concat-cons, append nil sq, decidable le, filter iseg |
